(in-package "ACL2")

#| 
  permutations.lisp
  ~~~~~~~~~~~~~~~~~

In this book we develop the definition of permutation, and justify that
permutation is an equivalence relation. We also prove some properties relating
to congruences of permutations with other functions. This is by no means an
adequate theory on permutations to gain the status of a reusable book. However,
the proof on equivalence of permutations is interesting because I base the
proof on simple equality reasoning.
|#

(defun memberp (e x)
  (if (endp x) nil
    (if (equal e (first x)) T
      (memberp e (rest x)))))

(defun my-del (e x)
  (if (endp x) nil
    (if (equal e (first x))
	(rest x)
      (cons (first x) (my-del e (rest x))))))

(defun perm (x y)
  (if (endp x) (endp y)
    (and (memberp (first x) y)
	 (perm (rest x) (my-del (first x) y)))))

;create-y
;input: (create-y 110 '(111 112 113))
;output: ((110 . 111) (110 . 112) (110 . 113))
(defun create-y (x ys)
  (if (consp ys)
      (cons (cons x (car ys)) (create-y x (cdr ys)))
      nil)
  )

;create=x
;input: (create-x '(110 111 112) '(113 114 115))
;output: (((110 . 113) (110 . 114) (110 . 115)) ((111 . 113) (111 . 114) (111 . 115)) ((112 . 113) (112 . 114) (112 . 115)))
(defun create-x (xs ys)
  (if (consp xs)
      (cons (create-y (car xs) ys) (create-x (cdr xs) ys))
      nil
     )
  )

;create-all-possible-combinations
(defun create-all-possible-combinations (xs ys)
  (create-x xs ys)       
  )